as:(top List), f:top. ((null(as)))  sqequal(last(map(f; as)); (f(last(as)))) 

latex

Definitions	t  T, top, x:A. B(x), ||as||, A  B, P  Q, lelt(i; j; k), P  Q, False, A, int_seg(i; j), last(L), null(as), b, ge(i; j), prop{i:l}, P  Q
Lemmas	not functionality wrt iff, assert of null, pos length, not wf, assert wf, null wf3, length-map, select-map, le wf, length wf1, top wf